(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 2))
(let ((e4 15))
(let ((e5 (+ v2 v1)))
(let ((e6 (- v1 v2)))
(let ((e7 (* v2 e6)))
(let ((e8 (/ e3 (- e3))))
(let ((e9 (/ e4 e4)))
(let ((e10 (* e6 v1)))
(let ((e11 (+ v1 v1)))
(let ((e12 (- v2 e11)))
(let ((e13 (* e12 (- e3))))
(let ((e14 (/ e4 (- e3))))
(let ((e15 (/ e3 e4)))
(let ((e16 (+ e10 v1)))
(let ((e17 (+ e10 e6)))
(let ((e18 (- e8 e12)))
(let ((e19 (- e15)))
(let ((e20 (+ e9 e17)))
(let ((e21 (- e19 e15)))
(let ((e22 (* v2 e20)))
(let ((e23 (- e14)))
(let ((e24 (- e22 e7)))
(let ((e25 (* e19 v2)))
(let ((e26 (+ e12 e16)))
(let ((e27 (+ e24 e19)))
(let ((e28 (* e12 e4)))
(let ((e29 (/ e4 (- e3))))
(let ((e30 (- e5)))
(let ((e31 (* e25 e21)))
(let ((e32 (/ e4 e4)))
(let ((e33 (* e12 e26)))
(let ((e34 (- e6 e21)))
(let ((e35 (- e9 e20)))
(let ((e36 (+ e19 v1)))
(let ((e37 (+ e21 e22)))
(let ((e38 (/ e4 e4)))
(let ((e39 (- v2)))
(let ((e40 (- e16)))
(let ((e41 (+ e8 v0)))
(let ((e42 (distinct e32 e20)))
(let ((e43 (>= e26 v2)))
(let ((e44 (<= e15 e25)))
(let ((e45 (= e32 e23)))
(let ((e46 (distinct e31 e21)))
(let ((e47 (<= e25 e28)))
(let ((e48 (<= e24 e39)))
(let ((e49 (> e39 e37)))
(let ((e50 (>= e31 e29)))
(let ((e51 (distinct e6 e36)))
(let ((e52 (= e15 e11)))
(let ((e53 (<= e21 e35)))
(let ((e54 (<= e22 v2)))
(let ((e55 (>= e11 e27)))
(let ((e56 (distinct e27 e8)))
(let ((e57 (distinct e30 e37)))
(let ((e58 (< e12 v1)))
(let ((e59 (distinct e21 e26)))
(let ((e60 (>= e14 e27)))
(let ((e61 (<= e26 e9)))
(let ((e62 (distinct e29 e24)))
(let ((e63 (> e23 e32)))
(let ((e64 (>= e30 e31)))
(let ((e65 (> e27 e35)))
(let ((e66 (>= e12 e37)))
(let ((e67 (distinct e20 e20)))
(let ((e68 (> e13 e5)))
(let ((e69 (>= v1 e30)))
(let ((e70 (>= e6 e24)))
(let ((e71 (= e39 e18)))
(let ((e72 (> e30 e39)))
(let ((e73 (> e18 e31)))
(let ((e74 (distinct e18 e30)))
(let ((e75 (= e31 e21)))
(let ((e76 (distinct e28 e32)))
(let ((e77 (distinct e12 e11)))
(let ((e78 (< v0 e33)))
(let ((e79 (> e22 e12)))
(let ((e80 (> e24 e27)))
(let ((e81 (distinct e7 e9)))
(let ((e82 (> e32 v1)))
(let ((e83 (<= e32 e32)))
(let ((e84 (< e30 e6)))
(let ((e85 (<= e10 e10)))
(let ((e86 (<= e6 e14)))
(let ((e87 (> e40 e33)))
(let ((e88 (> e13 v0)))
(let ((e89 (>= e18 v1)))
(let ((e90 (= e10 v1)))
(let ((e91 (< e29 e9)))
(let ((e92 (<= e34 e41)))
(let ((e93 (distinct e7 e21)))
(let ((e94 (<= e6 e19)))
(let ((e95 (<= e27 e41)))
(let ((e96 (= e17 v2)))
(let ((e97 (> e19 e28)))
(let ((e98 (< e41 e36)))
(let ((e99 (< e38 e9)))
(let ((e100 (= e15 e23)))
(let ((e101 (>= e35 v1)))
(let ((e102 (<= e20 e28)))
(let ((e103 (>= v0 e35)))
(let ((e104 (<= e22 e18)))
(let ((e105 (< e7 e8)))
(let ((e106 (distinct e36 e35)))
(let ((e107 (= e13 e15)))
(let ((e108 (>= e30 e5)))
(let ((e109 (>= e28 e34)))
(let ((e110 (> e40 e8)))
(let ((e111 (< e5 e10)))
(let ((e112 (distinct e20 e8)))
(let ((e113 (> e10 e25)))
(let ((e114 (>= e23 v1)))
(let ((e115 (>= e14 e40)))
(let ((e116 (>= e18 e14)))
(let ((e117 (distinct e8 e14)))
(let ((e118 (distinct e41 e10)))
(let ((e119 (< e27 e41)))
(let ((e120 (> e27 e37)))
(let ((e121 (< e11 e17)))
(let ((e122 (> e15 e27)))
(let ((e123 (= e37 e32)))
(let ((e124 (< v0 e20)))
(let ((e125 (<= e30 e26)))
(let ((e126 (= e8 e37)))
(let ((e127 (> e17 e31)))
(let ((e128 (< e6 e16)))
(let ((e129 (>= e36 e14)))
(let ((e130 (> e19 e11)))
(let ((e131 (<= e11 e23)))
(let ((e132 (= e35 e27)))
(let ((e133 (> e34 e34)))
(let ((e134 (distinct e19 e30)))
(let ((e135 (= e8 e20)))
(let ((e136 (< e32 e11)))
(let ((e137 (>= e32 e38)))
(let ((e138 (> e19 e6)))
(let ((e139 (= e18 e6)))
(let ((e140 (> e25 v2)))
(let ((e141 (<= e22 e16)))
(let ((e142 (< e6 e21)))
(let ((e143 (= e28 e26)))
(let ((e144 (> e17 e26)))
(let ((e145 (> e28 e33)))
(let ((e146 (>= e18 e16)))
(let ((e147 (< e12 e16)))
(let ((e148 (distinct e30 e6)))
(let ((e149 (= e34 e28)))
(let ((e150 (<= e11 v1)))
(let ((e151 (distinct e32 e14)))
(let ((e152 (distinct e33 e35)))
(let ((e153 (< e7 e10)))
(let ((e154 (distinct e31 e16)))
(let ((e155 (< e33 e26)))
(let ((e156 (>= e24 e21)))
(let ((e157 (distinct e37 e19)))
(let ((e158 (= e9 e28)))
(let ((e159 (= v1 e29)))
(let ((e160 (<= e25 e6)))
(let ((e161 (< e10 e7)))
(let ((e162 (> e14 e30)))
(let ((e163 (> e38 v1)))
(let ((e164 (distinct e6 e38)))
(let ((e165 (>= e18 e34)))
(let ((e166 (< e7 e5)))
(let ((e167 (= e15 e40)))
(let ((e168 (= e32 e6)))
(let ((e169 (distinct e41 e20)))
(let ((e170 (>= v0 e20)))
(let ((e171 (<= e7 e5)))
(let ((e172 (> e26 e39)))
(let ((e173 (< e29 e8)))
(let ((e174 (>= e41 e13)))
(let ((e175 (and e57 e149)))
(let ((e176 (= e165 e102)))
(let ((e177 (=> e169 e108)))
(let ((e178 (and e47 e58)))
(let ((e179 (not e171)))
(let ((e180 (or e179 e125)))
(let ((e181 (and e92 e110)))
(let ((e182 (= e87 e121)))
(let ((e183 (ite e126 e122 e132)))
(let ((e184 (not e55)))
(let ((e185 (=> e54 e82)))
(let ((e186 (ite e136 e123 e51)))
(let ((e187 (and e86 e147)))
(let ((e188 (and e91 e133)))
(let ((e189 (ite e94 e181 e63)))
(let ((e190 (ite e46 e148 e120)))
(let ((e191 (or e67 e66)))
(let ((e192 (= e61 e77)))
(let ((e193 (xor e83 e81)))
(let ((e194 (xor e135 e175)))
(let ((e195 (and e162 e89)))
(let ((e196 (=> e56 e79)))
(let ((e197 (xor e53 e103)))
(let ((e198 (not e114)))
(let ((e199 (ite e80 e128 e52)))
(let ((e200 (= e74 e64)))
(let ((e201 (and e97 e174)))
(let ((e202 (=> e104 e70)))
(let ((e203 (not e150)))
(let ((e204 (or e151 e134)))
(let ((e205 (not e84)))
(let ((e206 (ite e193 e75 e168)))
(let ((e207 (xor e154 e160)))
(let ((e208 (not e163)))
(let ((e209 (and e144 e42)))
(let ((e210 (or e76 e177)))
(let ((e211 (=> e93 e173)))
(let ((e212 (= e111 e184)))
(let ((e213 (ite e164 e158 e180)))
(let ((e214 (not e96)))
(let ((e215 (not e189)))
(let ((e216 (ite e124 e141 e202)))
(let ((e217 (ite e50 e44 e44)))
(let ((e218 (ite e65 e107 e152)))
(let ((e219 (= e206 e101)))
(let ((e220 (ite e157 e178 e142)))
(let ((e221 (not e208)))
(let ((e222 (ite e218 e137 e198)))
(let ((e223 (and e190 e159)))
(let ((e224 (=> e183 e176)))
(let ((e225 (xor e197 e212)))
(let ((e226 (ite e68 e156 e201)))
(let ((e227 (=> e224 e99)))
(let ((e228 (ite e49 e129 e43)))
(let ((e229 (= e88 e211)))
(let ((e230 (ite e200 e161 e215)))
(let ((e231 (or e145 e113)))
(let ((e232 (xor e106 e195)))
(let ((e233 (not e217)))
(let ((e234 (xor e204 e182)))
(let ((e235 (not e172)))
(let ((e236 (ite e45 e188 e130)))
(let ((e237 (and e138 e205)))
(let ((e238 (not e191)))
(let ((e239 (xor e194 e186)))
(let ((e240 (= e227 e170)))
(let ((e241 (or e207 e73)))
(let ((e242 (=> e139 e235)))
(let ((e243 (ite e192 e60 e155)))
(let ((e244 (or e140 e225)))
(let ((e245 (= e238 e95)))
(let ((e246 (or e231 e100)))
(let ((e247 (not e98)))
(let ((e248 (ite e127 e241 e116)))
(let ((e249 (=> e115 e244)))
(let ((e250 (not e85)))
(let ((e251 (=> e226 e203)))
(let ((e252 (or e109 e72)))
(let ((e253 (or e146 e69)))
(let ((e254 (=> e185 e237)))
(let ((e255 (and e230 e253)))
(let ((e256 (= e252 e232)))
(let ((e257 (and e236 e243)))
(let ((e258 (ite e242 e210 e257)))
(let ((e259 (ite e153 e187 e229)))
(let ((e260 (xor e246 e239)))
(let ((e261 (ite e249 e78 e258)))
(let ((e262 (xor e214 e118)))
(let ((e263 (= e119 e199)))
(let ((e264 (and e220 e62)))
(let ((e265 (=> e221 e254)))
(let ((e266 (= e196 e222)))
(let ((e267 (or e131 e131)))
(let ((e268 (= e105 e248)))
(let ((e269 (xor e167 e59)))
(let ((e270 (ite e223 e256 e223)))
(let ((e271 (and e263 e264)))
(let ((e272 (xor e267 e255)))
(let ((e273 (not e271)))
(let ((e274 (not e213)))
(let ((e275 (= e233 e228)))
(let ((e276 (not e250)))
(let ((e277 (xor e266 e219)))
(let ((e278 (=> e251 e276)))
(let ((e279 (ite e166 e268 e259)))
(let ((e280 (ite e71 e260 e260)))
(let ((e281 (or e279 e234)))
(let ((e282 (ite e280 e278 e274)))
(let ((e283 (or e262 e117)))
(let ((e284 (=> e240 e281)))
(let ((e285 (= e272 e48)))
(let ((e286 (not e143)))
(let ((e287 (not e209)))
(let ((e288 (= e283 e245)))
(let ((e289 (ite e112 e273 e90)))
(let ((e290 (ite e247 e269 e269)))
(let ((e291 (not e285)))
(let ((e292 (or e290 e290)))
(let ((e293 (= e291 e291)))
(let ((e294 (=> e275 e286)))
(let ((e295 (ite e288 e287 e289)))
(let ((e296 (=> e294 e277)))
(let ((e297 (or e295 e284)))
(let ((e298 (and e296 e261)))
(let ((e299 (xor e216 e216)))
(let ((e300 (not e282)))
(let ((e301 (not e299)))
(let ((e302 (and e293 e265)))
(let ((e303 (ite e301 e292 e301)))
(let ((e304 (or e302 e300)))
(let ((e305 (=> e303 e303)))
(let ((e306 (ite e304 e297 e304)))
(let ((e307 (and e298 e305)))
(let ((e308 (xor e306 e270)))
(let ((e309 (= e308 e308)))
(let ((e310 (= e307 e309)))
e310
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
